\begin{tabbing}
$\forall$\=$E$:Type, ${\it dE}$:EqDecider($E$), ${\it dL}$:EqDecider(IdLnk), $V$:(Knd$\rightarrow$Id$\rightarrow$Type), ${\it pred?}$:($E$$\rightarrow$(?$E$)),\+
\\[0ex]${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id))), ${\it val}$:($e$:$E$$\rightarrow$$V$(kind($e$),loc($e$))),
\\[0ex]$p$:(\=$\forall$$e$:$E$, $l$:IdLnk.\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex]($\forall$${\it e''}$:$E$.
\\[0ex]($\uparrow$rcv?(${\it e''}$))
\\[0ex]$\Rightarrow$ (sender(${\it e''}$) = $e$)
\\[0ex]$\Rightarrow$ (link(${\it e''}$) = $l$)
\\[0ex]$\Rightarrow$ (((${\it e''}$ = ${\it e'}$) $\vee$ ${\it e''}$ $<$ ${\it e'}$) \& loc(${\it e'}$) = destination($l$) $\in$ Id))), $e$:$E$, $l$:IdLnk.
\-\-\-\\[0ex]SWellFounded(($\neg$($\uparrow$first($y$))) c$\wedge$ ($x$ = pred($y$) $\in$ $E$))
\\[0ex]$\Rightarrow$ (sends(${\it dE}$;${\it dL}$;${\it pred?}$;${\it info}$;${\it val}$;$p$;$e$;$l$) $\in$ (Msg($\lambda$$l$,${\it tg}$. $V$(rcv($l$,${\it tg}$),destination($l$))) List))
\end{tabbing}